
/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.api;

// should be able to remove many of these
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;

import alloy.ast.Command;
import alloy.ast.Decl;
import alloy.ast.FindCommand;
import alloy.ast.Formula;
import alloy.ast.Id;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.Module;
import alloy.ast.Multiplicity;
import alloy.ast.Node;
import alloy.ast.QualifiedName;
import alloy.ast.SigExpr;
import alloy.ast.Signature;
import alloy.ast.Specification;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.bool.BooleanFormula;
import alloy.transform.FunctionSkolemizer;
import alloy.transform.atomize.AtomizationState;
import alloy.transl.ExprTransl;
import alloy.transl.TranslInfo;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.ScopedType;
import alloy.type.SigType;
import alloy.type.UnionType;
import alloy.util.Dbg;
import alloy.util.MultiDimIter;
import alloy.viz.alloyviz.AlloyAtom;
import alloy.viz.alloyviz.AlloyModule;
import alloy.viz.alloyviz.AlloyRelation;
import alloy.viz.alloyviz.AlloySet;
import alloy.viz.alloyviz.AlloyTuple;
import alloy.viz.alloyviz.AlloyType;
import alloy.viz.alloyviz.TypeStructure;

/** Represents one instance of an Alloy formula. */
public class Instance extends SolutionDataImpl {

    /** info from atomization -- see comment there in AtomizationVisitor */
    private Map _atomizedIdToOldLeafExpr;

    /** The {@link TranslInfo} used during translation.  It can be queried for various
    summary information about the formula, e.g. the list of all relations.
    @see #getTranslator */
//    private TranslInfo _translator;

    /** Assignment of Boolean variables to values */
    private boolean[] _solution;

    /** The desugared Alloy formula we were analyzing */
//    private Formula _formula;

    /** The {@link Command} we were analyzing. */
    private Command _command;

    /** The translation of the formula we were analyzing */
//    private BooleanFormula _translation;

    /** Mapping from LeafExprs in original formula to their values */
    // LeafId -> Relation
    private Map _oldLeafIdToRelation;

    /** list of leaf exprs prior to atomization */
    private List _oldLeafExprs = new ArrayList();

    /** subset of _oldLeafExprs that are SigExprs */
    private List _oldSigExprs = new ArrayList();

    /** subset of _oldLeafExprs that are skolem VariableExprs */
    private List _oldSkolems = new ArrayList();

    /** map from Atom's to the deepest BasicType they are a member of **/
    private Map _atomToBasicType = new HashMap();

    /**
     * Atom -> (field LeafId->Relation)
     */
    private Map _atomToFieldValues = new HashMap();

    /**
     * Atom -> Set(field LeafExpr's)
     */
    //private Map _atomToFieldExprs = new HashMap();

    private Set conflictNames = new HashSet();

    private String stringRep = "";

    /** map from types (SigTypes and the one IntType and EmptyType) to their
     * lists of Atom's.  This is stored because
     * every new execution calls ScopedType.setScope and the previous lists
     * of atoms are gone.  However, we need to retain that information to
     * get the correct deatomized atom names.
     * <p>
     * Note: it is *incorrect* to use _typeToAtomList to produce an iterator of 
     * atoms of each type because the atom lists are generated during translation
     * with a size equal to the type's scope.  Hence, the solution may contain
     * less atoms for the type than its scope requires, in which case, some 
     * of the atoms in the atom list are not referenced and should not be used. 
     */
    private Map _typeToAtomList = new HashMap();

    // alloy.api.Atom -> alloy.viz.alloyviz.AlloyAtom
    private Map _atomToAlyAtom = new HashMap();

    //  a map from old LeafId's to a Set containing their viz api elements
    // a Set is needed for splitting up union types
    private Map _oldLeafIdsToVizElts = new HashMap();

    public Instance(
        TranslInfo translator_,
        boolean[] solution_,
        Formula formula_,
        Command command_,
        BooleanFormula translation_,
        Specification spec_,
        FunctionSkolemizer fs_) {
        super(translator_, solution_, formula_, command_, translation_, spec_, fs_);
//        _translator = translator_;
        _solution = solution_;
//        _formula = formula_;
        _command = command_;
//        _translation = translation_;

        Dbg.chk(
            _command instanceof FindCommand,
            "SolutionData got passed a command that's not a FindCommand");
        //AtomizationInfo atomizationInfo = ((FindCommand)_command).atomizationInfo;
        _atomizedIdToOldLeafExpr = AtomizationState.getAtomizedIdToOldLeafExpr((FindCommand)_command); //atomizationInfo._atomizedIdToOldLeafExpr;

        // initialize _typeToAtomList

        // get SigType atom lists
        for (Iterator typeIter = _command.stringToType.values().iterator(); typeIter.hasNext();) {
            SigType type = (SigType)typeIter.next();
            _typeToAtomList.put(type, type.getAtomList());
        }

        // get IntType list
        BasicType iType = this.getIntType();
        if (iType != null) {
            _typeToAtomList.put(iType, ((ScopedType)iType).getAtomList());
        }

        Map exprsToTransls = translator_.getRelationExprsToTransls();

        // temporary map.  it is used to generate the _oldLeafExprs list.  The reason we need
        // this map, instead of simply using a Set to avoid repeats, is that the same oldLeafExpr
        // (by LeafId) may appear multiple times in _atomizedIdToOldLeafExpr, they aren't 
        // necessarily Object.equals() to each other, and could be repeated in a Set.
        Map idToLeafExpr = new HashMap();

        for (Iterator iter = _atomizedIdToOldLeafExpr.entrySet().iterator(); iter.hasNext();) {
            Map.Entry entry = (Map.Entry)iter.next();
            LeafExpr leafExpr = (LeafExpr)entry.getValue();
            if (!idToLeafExpr.containsKey(leafExpr.getLeafId())) {
                //System.out.println(
                //  "Adding relation to old leaf expr list: " + leafExpr.nodeString());
                idToLeafExpr.put(leafExpr.getLeafId(), leafExpr);
            }
        }

        _oldLeafExprs = new ArrayList(idToLeafExpr.values());

        Collections.sort(_oldLeafExprs);
        _oldLeafExprs = Collections.unmodifiableList(_oldLeafExprs);
        
        for (Iterator iter = _oldLeafExprs.iterator(); iter.hasNext();) {
            Object expr = iter.next();
            if (expr instanceof SigExpr) {
                _oldSigExprs.add(expr);
            }
        }

        for (Iterator iter = _oldLeafExprs.iterator(); iter.hasNext();) {
            LeafExpr expr = (LeafExpr)iter.next();
            if (expr instanceof VariableExpr && !isField(expr)) {
                _oldSkolems.add(expr);
            }
        }

        // add to _atomizedIdToOldLeafExpr self-mapping for non-atomized relations
        Iterator entryIter = exprsToTransls.entrySet().iterator();
        while (entryIter.hasNext()) {
            Map.Entry entry = (Map.Entry)entryIter.next();
            LeafExpr leafExpr = (LeafExpr)entry.getKey();
//            ExprTransl leafTransl = (ExprTransl)entry.getValue();

            LeafExpr oldLeafExpr = (LeafExpr)_atomizedIdToOldLeafExpr.get(leafExpr.getLeafId());
            if (oldLeafExpr == null) {
                // leafExpr was not one generated by the atomizer (i.e. it was in the original
                // model but didn't need to be atomized).  we create a self-mapping for it.                
                _atomizedIdToOldLeafExpr.put(leafExpr.getLeafId(), leafExpr);

            }
        }

        // set up empty relations in _oldLeafIdToRelation
        _oldLeafIdToRelation = new HashMap();
        for (Iterator iter = _oldLeafExprs.iterator(); iter.hasNext();) {
            LeafExpr oldLeafExpr = (LeafExpr)iter.next();
            LeafId oldLeafId = oldLeafExpr.getLeafId();
            if (!_oldLeafIdToRelation.containsKey(oldLeafId)) {
                //System.out.println("Creating relation for " + oldLeafExpr.nodeString());
                _oldLeafIdToRelation.put(oldLeafId, new Relation());
            }
        }
        // set up a Relation for the IntType if it's present in this model
	/** EMINA:  NO LONGER NEEDS A SPECIAL CASE ?  **/

        if (this.getIntType() != null) {
            _oldLeafIdToRelation.put(getIntId(), new Relation());
        }	

        // construct deatomized relations, by summing contributions from atomized versions
        entryIter = exprsToTransls.entrySet().iterator();
        while (entryIter.hasNext()) {
            Map.Entry entry = (Map.Entry)entryIter.next();
            LeafExpr leafExpr = (LeafExpr)entry.getKey();
            ExprTransl leafTransl = (ExprTransl)entry.getValue();

            LeafExpr oldLeafExpr = (LeafExpr)_atomizedIdToOldLeafExpr.get(leafExpr.getLeafId());                      
            Dbg.chk(oldLeafExpr, "Translated expr not associated with original leaf expr");
            
            // bug fix for empty abstract type instances (including univ, see comment for 
            // _atomizedIdToOldLeafExpr in alloy.transform.AtomizationVisitor for more info
            // makes sure abstract ancestors are populated correctly
            // only need to do this for the atomic type SigExpr's (e.g. don't need to do it
            // for their subtypes which became subsets, and obviously the atomic types'
            // supertypes never appear in exprsToTransls, which is why this fix is 
            // here to populate them in the first place)
            if (oldLeafExpr instanceof SigExpr && 
                !isSubset((SigExpr)oldLeafExpr) && // only applies for types
                isAtomicTypeExpr((SigExpr)leafExpr)) { // only atomic (including atomic remainder) types
                // populate this type and every ancestor of this type with the 
                // atoms in this leafTransl
                
                SigType currentType = oldLeafExpr.getType().toRelationType().getSigType();
                
                while (currentType!=null) {
                    LeafId currentTypeId = currentType.getSignature().getLeafId();            
                    Relation relation = (Relation)_oldLeafIdToRelation.get(currentTypeId);
                    Dbg.chk(relation, "No relation associated with original leaf expr");                        
                    // add interpretation of leafTransl to currentType
                    _interpretRelation(leafTransl, _solution, relation);
                    
                    currentType = currentType.getSuperType();                                       
                }                                
            }
            else {            

                Relation relation = (Relation)_oldLeafIdToRelation.get(oldLeafExpr.getLeafId());
    
                Dbg.chk(relation, "No relation associated with original leaf expr");                        
    
                // add interpretation of leafTransl to the relation associated with the original leafExpr
                _interpretRelation(leafTransl, _solution, relation);
            }
        }
        
        // recursively do the atom name changing in a depth first manner
//        Set modifiedAtoms = new HashSet();
        Set topLevel = new HashSet();
        for (Iterator typesIter = SigType.getSigTypes().iterator(); typesIter.hasNext();) {
            SigType sig = (SigType)typesIter.next();
            if (sig.getSuperType() == null) {
                // top-level types are explored first
                topLevel.add(sig);
            }
        }
        convertAtoms(topLevel, new HashSet());

        if (this.getIntType() != null) {
            convertIntAtoms();
        }

        computeShortSigNames(_oldSigExprs);

        
        

        // make sure each atom has an atomToFieldValues map for every applicable field 
        // (even if it's an empty).
        for (Iterator atomIter = _atomToBasicType.keySet().iterator(); atomIter.hasNext();) {
            Atom atom = (Atom)atomIter.next();
            _atomToFieldValues.put(atom, new HashMap());
        }

        for (Iterator oldLeafIter = _oldLeafExprs.iterator(); oldLeafIter.hasNext();) {
            LeafExpr oldLeafExpr = (LeafExpr)oldLeafIter.next();

            Relation relation = (Relation)_oldLeafIdToRelation.get(oldLeafExpr.getLeafId());

            // extract info from the relation if this is a field
            if (isField(oldLeafExpr)) {
                for (Iterator tuples = relation.tuples(); tuples.hasNext();) {
                    Tuple tup = (Tuple)tuples.next();
                    Tuple newTup = new Tuple();

                    Iterator atoms = tup.atoms();

                    Atom firstAtom = (Atom)atoms.next();

                    // should definitely have at least one more element because
                    // these are fields
                    Dbg.chk(atoms.hasNext());
                    while (atoms.hasNext()) {
                        newTup.add((Atom)atoms.next());
                    }
                    
                    // record the value(s) of the field
                    Map fieldToVals = (Map)_atomToFieldValues.get(firstAtom);
                    if (fieldToVals == null) {
                        System.out.println("Unexpected atom-to-field mapping failure in alloy.api.Instance!");
                        fieldToVals = new HashMap();
                        _atomToFieldValues.put(firstAtom, fieldToVals);
                    }

                    Relation rel = (Relation)fieldToVals.get(oldLeafExpr.getLeafId());
                    if (rel == null) {
                        rel = new Relation();
                        fieldToVals.put(oldLeafExpr.getLeafId(), rel);
                    }
                    rel.add(newTup);

                }
            }
        }

        
    }
    
    /**
     * 
     * @param atomizedExpr expr from exprsToTransl
     * @return true if atomizedExpr corresponds to the SigExpr of an atomic type
     * (including  atomic remainder types)
     */
    private boolean isAtomicTypeExpr(SigExpr atomizedExpr) {
        LeafExpr oldLeafExpr = (LeafExpr)_atomizedIdToOldLeafExpr.get(atomizedExpr.getLeafId());
        LeafId oldLeafId = oldLeafExpr.getLeafId();
        
        // simple atomic type (not remainder)
        if (atomizedExpr.getLeafId().equals(oldLeafId)) {
            return true;
        }
        
        // if it's a atomic remainder, it'll map to its supertype, which is not atomic
        // and is an old expr that maps to itself
        SigType superType = atomizedExpr.getType().toRelationType().getSigType().getSuperType();        
        return (superType != null && 
                superType.getSignature().getLeafId().equals(oldLeafId) &&
                oldLeafId.equals(((LeafExpr)_atomizedIdToOldLeafExpr.get(oldLeafId)).getLeafId()));
        
    }

    /** Add interpretation of leafTransl to the relation associated with the original leafExpr */
    void _interpretRelation(ExprTransl leafTransl_, boolean[] solution_, Relation relation_) {
        for (Iterator indIter = new MultiDimIter(leafTransl_.getFormulas().getDims()); indIter.hasNext();) {
            int[] inds = (int[])indIter.next();
            BooleanFormula bf = leafTransl_.getTupleFormula(inds);
            if (bf.interpret(solution_)) {
                Tuple tuple = new alloy.api.Tuple();
                for (int i = 0; i < inds.length; i++) {
                    Dbg.chk(leafTransl_.getType(), "ExprTrans/interpret: no relation type");
                    //Atom atom = leafTransl_.getType().getBasicTypeAt(i).getAtom (inds[i]);
                    Atom atom =
                        (Atom) ((List)_typeToAtomList.get(leafTransl_.getType().getBasicTypeAt(i))).get(
                            inds[i]);
                    Dbg.chk(atom);
                    tuple.add(atom);
                }
                relation_.add(tuple);
            }
        }
        return;
    }

    private boolean isField(LeafExpr expr) {
        if (expr instanceof VariableExpr) {

            // a field's relaetion has to be at least binary--the first column is
            // the sig where the field was declared
            if (expr.getType().arity() == 1) {
                return false;
            }

            Iterator relTypeIter = expr.getType().getTypeIter();

            String fieldName = expr.nodeString();

            // iterate thru types.  If the field is found on the beginning column of
            // any of the types, we're set.
            while (relTypeIter.hasNext()) {
                RelationType relType = (RelationType)relTypeIter.next();
                SigType firstType = (SigType)relType.getBasicTypeAt(0);

                if (firstType.getSignature().getFieldLeafId(fieldName) != null) {
                    return true;
                }

            }

            return false;

        } else {
            return false;
        }
    }

    private LeafId getIntId() {
	return ((SigType) getIntType()).getSignature().getLeafId();
    }

    /**
     * fills in the atom name fields of Int atoms with the appropriate integer value
     */
    private void convertIntAtoms() {
        if (this.getIntType() != null) {
            Relation relation = (Relation)_oldLeafIdToRelation.get(getIntId());
            Dbg.chk(relation, "no relation created for Int");
            List intAtomList = (List)_typeToAtomList.get(getIntType());
            Dbg.chk(intAtomList, "no atom list for Int");

            for (Iterator ti = relation.tuples(); ti.hasNext();) {
                Tuple tuple = (Tuple)ti.next();
                for (Iterator ai = tuple.atoms(); ai.hasNext();) {
                    Atom atom = (Atom)ai.next();
                    int atomIndex = intAtomList.indexOf(atom);
                    Dbg.chk(atomIndex != -1, "cannot find atom in atom list");
                    long atomValue = this.getIntAtomValue(atomIndex);
                    atom.setName(Long.toString(atomValue));
                    _atomToBasicType.put(atom, this.getIntType());
                }
            }
        }
    }

    private void convertAtoms(Set sigTypes, Set modifiedAtoms) {
        for (Iterator typeIter = sigTypes.iterator(); typeIter.hasNext();) {
            SigType type = (SigType)typeIter.next();
            if ((SigType.getSigTypeForString(type.toString()) == null) || 
		(type == this.getIntType())) {
                // this is a SigType that was a subtype of another SigType but does not appear
                // in the global SigType tree.  Hence it must've been an atomized SigType.
                // we skip these so that the immediate supertype will correct them
		// we also skip Int atoms
                continue;
            }
            Set subtypes = type.getSubTypes();

            // recursive call on subtypes
            convertAtoms(subtypes, modifiedAtoms);

            // map current type
            SigExpr expr = (SigExpr) type.toExpr();
            expr.setLeafId(type.getSignature().getLeafId());
            Dbg.chk(expr);
            Relation relation = (Relation)_oldLeafIdToRelation.get(expr.getLeafId());
            int counter = 0;
            String sigName = getShortSigName(expr);
            for (Iterator ti = relation.tuples(); ti.hasNext();) {
                Tuple tuple = (Tuple)ti.next();
                for (Iterator ai = tuple.atoms(); ai.hasNext();) {
                    Atom atom = (Atom)ai.next();
                    if (modifiedAtoms.add(atom)) {
                        _atomToBasicType.put(atom, type);
                        atom.setName(sigName + "_" + counter);
                        counter++;
                    }
                }
            }
        }
    }

    public String toString() {
        
        if (!stringRep.equals("")) {
            return stringRep;
        }

        StringBuffer ret = new StringBuffer();

        // go up the ast tree until the top Specification node is found

        Node node = _command;
        while (!(node instanceof Specification)) {
            node = node.getParent();
            Dbg.chk(node, "problem generating text output -- cannot go up ast tree");
        }

        Specification spec = (Specification)node;

        // iterate through modules
        for (Iterator modIter = spec.getModules().getModuleIter(); modIter.hasNext();) {
            Module module = (Module)modIter.next();

            ret.append("module " + module.getName().nodeString() + "\n");

            // iterate through signatures

            for (Iterator sigIter = module.getSignatures().getSignatureIter(); sigIter.hasNext();) {
                Signature sig = (Signature)sigIter.next();

                StringBuffer sigInfo = new StringBuffer();
                sigInfo.append("sig " + sig.getName().getId().nodeString());

                if (sig.isSubset()) {

                    // sig A in B+C ...

                    sigInfo.append(" in ");
                    for (Iterator subsetIter = sig.getSubsets().getSigExprIter(); subsetIter.hasNext();) {
                        SigExpr subsetExpr = (SigExpr)subsetIter.next();
                        sigInfo.append(subsetExpr.getSig().getId().nodeString());
                        if (subsetIter.hasNext()) {
                            sigInfo.append("+");
                        }
                    }
                } else {

                    // sig A extends B, or just sig A

                    Iterator extendsIter = sig.getExtends().getSigExprIter();
                    if (extendsIter.hasNext()) {
                        sigInfo.append(
                            " extends " + ((SigExpr)extendsIter.next()).getSig().getId().nodeString());
                    }
                }

                // add atoms of this sig
                Relation sigAtoms = getRelation(sig.getLeafId());

                sigInfo.append(" = " + (sig.getMult().equals(Multiplicity.ONE) ? "" : "{"));

                List sortedAtoms = new ArrayList();

                for (Iterator tuples = sigAtoms.tuples(); tuples.hasNext();) {
                    sortedAtoms.add(((Tuple)tuples.next()).atoms().next());

                }

                Collections.sort(sortedAtoms);

                for (Iterator atomsIter = sortedAtoms.iterator(); atomsIter.hasNext();) {
                    sigInfo.append(((Atom)atomsIter.next()).toString());
                    if (atomsIter.hasNext()) {
                        sigInfo.append(", ");
                    }
                }
                sigInfo.append((sig.getMult().equals(Multiplicity.ONE) ? "" : "}") + "\n");

                // iteratore through fields

                for (Iterator declIter = sig.getDecls().getDeclIter(); declIter.hasNext();) {
                    Decl decl = (Decl)declIter.next();

                    // need to do it separately for each variable in a Decl, e.g.
                    // sig A { foo, fee: F }

                    for (Iterator varsIter = decl.getVariables().getVariableIter(); varsIter.hasNext();) {

                        Variable var = (Variable)varsIter.next();

                        sigInfo.append("  " + var + " : " + decl.getExpr() + " = \n    {");

                        // print values in the form of A1 -> B1, A2 -> B2
                        // cluster tuples if originating from the same atom

                        // contains mappings like
                        // A1     Set("B1")
                        // A2     Set("B2", "B3")
                        // for higher-arity rels
                        // A1     Set("B1 -> C1", "B2 -> C2")

                        Map startAtomToStrings = new HashMap();

                        Relation fieldVals = getRelation(sig.getFieldLeafId(var.nodeString()));

                        for (Iterator tuples = fieldVals.tuples(); tuples.hasNext();) {
                            Iterator atoms = ((Tuple)tuples.next()).atoms();

                            Atom firstAtom = (Atom)atoms.next();

                            StringBuffer tupleString = new StringBuffer();
                            while (atoms.hasNext()) {
                                Atom next = (Atom)atoms.next();
                                tupleString.append(next);
                                if (atoms.hasNext()) {
                                    tupleString.append(" -> ");
                                }
                            }

                            Set storedStrings = (Set)startAtomToStrings.get(firstAtom);
                            if (storedStrings == null) {
                                storedStrings = new HashSet();
                                startAtomToStrings.put(firstAtom, storedStrings);
                            }
                            storedStrings.add(tupleString.toString());
                        }

                        List startAtoms = new ArrayList(startAtomToStrings.keySet());
                        Collections.sort(startAtoms);

                        for (Iterator startIter = startAtoms.iterator(); startIter.hasNext();) {
                            Atom startAtom = (Atom)startIter.next();

                            Set tuples = (Set)startAtomToStrings.get(startAtom);

                            sigInfo.append(startAtom.toString() + " -> " + (tuples.size() > 1 ? "{" : ""));

                            List sortedTuples = new ArrayList(tuples);
                            Collections.sort(sortedTuples);

                            for (Iterator tupIter = sortedTuples.iterator(); tupIter.hasNext();) {
                                sigInfo.append(tupIter.next());
                                if (tupIter.hasNext()) {
                                    sigInfo.append(", ");
                                }
                            }

                            if (tuples.size() > 1) {
                                sigInfo.append("}");
                            }

                            if (startIter.hasNext()) {
                                sigInfo.append(", \n     ");
                            }

                        }

                        sigInfo.append("}\n");

                        // end var

                    }

                    // end decl
                }

                ret.append(sigInfo);

                // end sig
            }

            // end module

            if (modIter.hasNext()) {
                ret.append("\n");
            }
        }

        // add skolems

        List skolems = getSkolems();
        if (!skolems.isEmpty()) {
            ret.append("\nskolem constants\n");
            for (Iterator skolemIter = skolems.iterator(); skolemIter.hasNext();) {
                VariableExpr skolem = (VariableExpr)skolemIter.next();
                String skolemName = shortenSkolem(skolem.nodeString());

                ret.append(skolemName + " = \n    {");

                Map startAtomToStrings = new HashMap();

                Relation skolemVals = getRelation(skolem.getLeafId());

                for (Iterator tuples = skolemVals.tuples(); tuples.hasNext();) {
                    Iterator atoms = ((Tuple)tuples.next()).atoms();

                    Atom firstAtom = (Atom)atoms.next();

                    if (atoms.hasNext()) {
                        // if it's at least binary...
                        StringBuffer tupleString = new StringBuffer();
                        while (atoms.hasNext()) {
                            Atom next = (Atom)atoms.next();
                            tupleString.append(next);
                            if (atoms.hasNext()) {
                                tupleString.append(" -> ");
                            }
                        }

                        Set storedStrings = (Set)startAtomToStrings.get(firstAtom);
                        if (storedStrings == null) {
                            storedStrings = new HashSet();
                            startAtomToStrings.put(firstAtom, storedStrings);
                        }
                        storedStrings.add(tupleString.toString());

                    }
                    if (startAtomToStrings.get(firstAtom)==null) {
                        startAtomToStrings.put(firstAtom,new HashSet());
                    }


                }

                List startAtoms = new ArrayList(startAtomToStrings.keySet());
                Collections.sort(startAtoms);

                for (Iterator startIter = startAtoms.iterator(); startIter.hasNext();) {
                    Atom startAtom = (Atom)startIter.next();

                    Set tuples = (Set)startAtomToStrings.get(startAtom);

                    ret.append(startAtom.toString());
                    if (tuples.size() > 0) {
                        // at least binary
                        ret.append(" -> " + (tuples.size() > 1 ? "{" : ""));
                    }

                    List sortedTuples = new ArrayList(tuples);
                    Collections.sort(sortedTuples);

                    for (Iterator tupIter = sortedTuples.iterator(); tupIter.hasNext();) {
                        ret.append(tupIter.next());
                        if (tupIter.hasNext()) {
                            ret.append(", ");
                        }
                    }

                    if (tuples.size() > 1) {
                        ret.append("}");
                    }

                    if (startIter.hasNext()) {
                        ret.append(", \n     ");
                    }

                }

                ret.append("}\n");

            }
        }

        stringRep = ret.toString();
        return stringRep;
    }

    public alloy.viz.alloyviz.VizInstance getVizInstance() {
        if (super.getVizInstance() != null) {
            return super.getVizInstance();
        }

        // a TypeStructure for the whole model (multiple modules).  will divide it
        // up later in the code
        TypeStructure ts = new TypeStructure();

        // module name -> Set(AlloyType, AlloySet, or AlloyRelation)
        Map modulesToVizElts = new HashMap();

        // a queue of old leafExpr's to examine
        LinkedList queue = new LinkedList(_oldLeafExprs);
        //System.out.println(queue.size() + 
        // include Int's SigExpr if necessary
        BasicType iType = this.getIntType();
        if (iType != null) {
            LeafExpr expr = iType.toExpr();
            expr.setLeafId(getIntId());
            queue.add(expr);
        }

        while (!queue.isEmpty()) {
            LeafExpr leaf = (LeafExpr)queue.removeFirst();
            if (leaf instanceof SigExpr && !isSubset((SigExpr)leaf)) {
                // a type
                String typeName = getShortSigName((SigExpr)leaf);
                BasicType basType = leaf.getType().toRelationType().getBasicTypeAt(0);

                AlloyType alyType = new AlloyType(typeName);
                Set dummy = new HashSet();
                dummy.add(alyType);
                _oldLeafIdsToVizElts.put(leaf.getLeafId(), dummy);

                String moduleName = getModuleName(leaf);
                Set elts = (Set)modulesToVizElts.get(moduleName);
                if (elts == null) {
                    elts = new HashSet();
                    modulesToVizElts.put(moduleName, elts);
                }
                elts.add(alyType);

            } else {
                // either a set or a relation

                // try to create an AlloySet or AlloyRelation, unless an AlloyType needed
                // hasn't been created--in that case put leaf at the back of queue

                UnionType leafType = leaf.getType();

                Set eltSet = new HashSet();
                boolean aborted = false;

                for (Iterator typeIter = leafType.getTypeIter(); typeIter.hasNext();) {

                    RelationType relType = (RelationType)typeIter.next();

                    if (relType.arity() == 1) {
                        // a set
                        BasicType setType = (BasicType)relType.getBasicTypeAt(0);

                        /** EMINA:  INT IS NOW A SIG TYPE**/
                        /**
                                    LeafId typeLeafId =
                            (setType instanceof IntType)
                            ? LeafId.INT_ID
                            : ((SigType)setType).getSignature().getLeafId();
                        **/
                        LeafId typeLeafId = ((SigType)setType).getSignature().getLeafId();

                        if (_oldLeafIdsToVizElts.get(typeLeafId) == null) {
                            // haven't created the type yet, enqueue this leaf
                            queue.add(leaf);
                            aborted = true;
                            break;
                        } else {
                            AlloyType alyType =
                                (AlloyType) ((Set)_oldLeafIdsToVizElts.get(typeLeafId)).iterator().next();
                            // create the AlloySet
                            String setName =
                                (leaf instanceof SigExpr)
                                    ? getShortSigName((SigExpr)leaf)
                                    : shortenSkolem(leaf.nodeString());
                            // this case is for unary skolems, which are VariableExprs
                            AlloySet alySet = new AlloySet(setName, alyType);
                            eltSet.add(alySet);

                        }
                    } else {
                        // A Relation
                        List alyTypes = new ArrayList();
                        for (Iterator typesIter = relType.getTypeIter(); typesIter.hasNext();) {
                            BasicType curType = (BasicType)typesIter.next();
                            //SigType curType = (SigType)typesIter.next();

                            /** EMINA:  INT IS NOW A SIG TYPE**/
                            /**
                                        LeafId typeLeafId =
                                            (curType instanceof IntType)
                                                ? LeafId.INT_ID
                                                : ((SigType)curType).getSignature().getLeafId();
                            **/
                            LeafId typeLeafId = ((SigType)curType).getSignature().getLeafId();

                            if (_oldLeafIdsToVizElts.get(typeLeafId) == null) {
                                // haven't created the type yet, enqueue this leaf
                                queue.add(leaf);
                                continue;
                            } else {
                                AlloyType alyType =
                                    (AlloyType) ((Set)_oldLeafIdsToVizElts.get(typeLeafId)).iterator().next();
                                // add to the List of types
                                alyTypes.add(alyType);
                            }
                        }
                        // create the AlloyRelation
                        String relName = shortenSkolem(leaf.nodeString());
                        AlloyRelation alyRel = new AlloyRelation(relName, alyTypes);
                        eltSet.add(alyRel);

                    }

                }

                if (!aborted) {
                    _oldLeafIdsToVizElts.put(leaf.getLeafId(), eltSet); 
                    String moduleName = getModuleName(leaf);
                    Set elts = (Set)modulesToVizElts.get(moduleName);
                    if (elts == null) {
                        elts = new HashSet();
                        modulesToVizElts.put(moduleName, elts);
                    }
                    for (Iterator eltIter = eltSet.iterator(); eltIter.hasNext();) {
                        elts.add(eltIter.next());
                    }
                }
            }
        }

        // generate typestructure for the entire model (across all modules)
        for (Iterator typesIter = SigType.getSigTypes().iterator(); typesIter.hasNext();) {
            SigType sigType = (SigType)typesIter.next();

            AlloyType type =
                (AlloyType) ((Set)_oldLeafIdsToVizElts.get(sigType.getSignature().getLeafId()))
                    .iterator()
                    .next();
            Dbg.chk(type);

            ts.addType(type);

            SigType superSigType = sigType.getSuperType();
            if (superSigType != null) {
                AlloyType superType =
                    (AlloyType) ((Set)_oldLeafIdsToVizElts.get(superSigType.getSignature().getLeafId()))
                        .iterator()
                        .next();
                Dbg.chk(superType);
                ts.addSuper(superType, type);
            }
        }

        List modules = new ArrayList();

        for (Iterator entryIter = modulesToVizElts.entrySet().iterator(); entryIter.hasNext();) {
            Map.Entry entry = (Map.Entry)entryIter.next();
            String moduleName = (String)entry.getKey();
            Set elts = (Set)entry.getValue();

            List sets = new ArrayList();
            List rels = new ArrayList();
            List types = new ArrayList();

            for (Iterator eltsIter = elts.iterator(); eltsIter.hasNext();) {
                Object elt = eltsIter.next();
                if (elt instanceof AlloyType) {
                    types.add(elt);
                } else if (elt instanceof AlloySet) {
                    sets.add(elt);
                } else {
                    rels.add(elt);
                }
            }

            AlloyModule mod = new AlloyModule(moduleName, types, sets, rels);
            modules.add(mod);

        }

        alloy.viz.alloyviz.Model model = new alloy.viz.alloyviz.Model(modules, ts, getModelName());
        alloy.viz.alloyviz.VizInstance vizInstance = new alloy.viz.alloyviz.VizInstance(model);

        LinkedList postponedIds = new LinkedList();

        for (Iterator idIter = _oldLeafIdToRelation.keySet().iterator(); idIter.hasNext();) {
            LeafId id = (LeafId)idIter.next();
            Object vizElt = ((Set)_oldLeafIdsToVizElts.get(id)).iterator().next();
            if (vizElt instanceof AlloyType) {
                // add atoms
                Relation rel = (Relation)_oldLeafIdToRelation.get(id);
                for (Iterator tupIter = rel.tuples(); tupIter.hasNext();) {
                    Tuple tup = (Tuple)tupIter.next();
                    Iterator atomIter = tup.atoms();
                    Atom atom = (Atom)atomIter.next();
                    Dbg.chk(!atomIter.hasNext()); // should not have any more atoms

                    // check if this is the deepest type the atom is a part of
                    // if not, then don't add it (only add once to the Instance)
                    BasicType basType = (BasicType)_atomToBasicType.get(atom);
                    Dbg.chk(basType);

                    if (getShortSigName((SigExpr)basType.toExpr()).equals(((AlloyType)vizElt).getName())) {
                        AlloyAtom alyAtom =
                            new AlloyAtom(atom.toString(), (AlloyType)vizElt, extractIndex(atom.toString()));
                        vizInstance.addAtom(alyAtom);
                        _atomToAlyAtom.put(atom, alyAtom);
                    }

                }
            } else {
                // a set or relation--we don't know if their atoms got added yet at this point
                // postone till all the types are done
                postponedIds.add(id);
            }
        }

        while (!postponedIds.isEmpty()) {
            LeafId id = (LeafId)postponedIds.removeFirst();
            Set eltSet = (Set)_oldLeafIdsToVizElts.get(id);
            Object vizElt = eltSet.iterator().next();
            if (vizElt instanceof AlloySet) {
                // a set
                Relation rel = (Relation)_oldLeafIdToRelation.get(id);
                for (Iterator tupIter = rel.tuples(); tupIter.hasNext();) {
                    Tuple tup = (Tuple)tupIter.next();
                    Iterator atomIter = tup.atoms();
                    Atom atom = (Atom)atomIter.next();
                    Dbg.chk(!atomIter.hasNext());
                    // should not have any more atoms, since set is unary
                    AlloyAtom alyAtom = (AlloyAtom)_atomToAlyAtom.get(atom);
                    Dbg.chk(alyAtom);

                    // if this set got partitioned, determine to which atom this
                    // atom belongs.  if the set didn't get partitioned, add to
                    // first AlloySet in eltSet w/o checking
                    if (eltSet.size() == 1) {
                        vizInstance.addAtomToSet(alyAtom, (AlloySet)vizElt);
                    } else {

                        AlloyType atomType = alyAtom.getType();
                        for (Iterator eltIter = eltSet.iterator(); eltIter.hasNext();) {
                            AlloySet curSet = (AlloySet)eltIter.next();
                            AlloyType curSetType = curSet.getType();

                            if (isSubtypeOf(ts, atomType, curSetType)) {
                                vizInstance.addAtomToSet(alyAtom, curSet);
                                break;
                            }
                        }
                    }
                }
            } else {
                // a relation
                Relation rel = (Relation)_oldLeafIdToRelation.get(id);
                for (Iterator tupIter = rel.tuples(); tupIter.hasNext();) {
                    Tuple tup = (Tuple)tupIter.next();
                    List alyAtoms = new ArrayList();

                    Iterator atomIter = tup.atoms();
                    while (atomIter.hasNext()) {
                        Atom atom = (Atom)atomIter.next();
                        AlloyAtom alyAtom = (AlloyAtom)_atomToAlyAtom.get(atom);
                        Dbg.chk(alyAtom);
                        alyAtoms.add(alyAtom);
                    }
                    AlloyTuple alyTup = new AlloyTuple(alyAtoms);

                    if (eltSet.size() == 1) {
                        vizInstance.addTupleToRelation(alyTup, (AlloyRelation)vizElt);
                    } else {
                        // relation got partitioned, so we need to determine to which partitioned
                        // part this tuple belongs.

                        // note: there's some amount of arbituaryness in this
                        // scheme.  suppose foo has type (A->B1->C) + (A->B->C1).
                        // Then the a tuple like (A_1, B1_1, C1_1) can belong to both.

                        for (Iterator eltIter = eltSet.iterator(); eltIter.hasNext();) {
                            AlloyRelation curRel = (AlloyRelation)eltIter.next();
                            boolean tupleOk = true;

                            Iterator tupAtomIter = alyTup.getAtoms().iterator();
                            for (Iterator relTypeIter = curRel.getTypes().iterator();
                                relTypeIter.hasNext();
                                ) {
                                AlloyType curRelType = (AlloyType)relTypeIter.next();
                                AlloyAtom curAtom = (AlloyAtom)tupAtomIter.next();
                                AlloyType curAtomType = curAtom.getType();
                                if (!isSubtypeOf(ts, curAtomType, curRelType)) {
                                    // failed
                                    tupleOk = false;
                                    break;
                                }
                            }

                            if (tupleOk) {
                                vizInstance.addTupleToRelation(alyTup, curRel);
                                break;
                            }

                        }
                    }

                }
            }
        }

        super.setVizInstance(vizInstance);
        return vizInstance;
    }

    private boolean isSubtypeOf(TypeStructure ts, AlloyType subType, AlloyType superType) {
        boolean hit = false;

        while (superType != null) {
            if (superType.equals(subType)) {
                hit = true;
                break;
            }
            superType = ts.getSuper(superType);
        }

        return hit;
    }

    private int extractIndex(String indexedName) {
        return Integer.parseInt(indexedName.substring(indexedName.lastIndexOf('_') + 1));
    }

    public String shortenSkolem(String fullName) {
        return fullName.substring(fullName.indexOf("@") + 1, fullName.length());
    }

    /*
     * from SigType.java
     */
    private void computeShortSigNames(Collection sigExprs) {

        conflictNames = new HashSet();
        Map id2qname = new HashMap(); // Id -> QualifiedName
        for (Iterator typeIter = sigExprs.iterator(); typeIter.hasNext();) {
            SigExpr sigExpr = (SigExpr)typeIter.next();
            QualifiedName qname = sigExpr.getSig();
            Id id = qname.getId();
            QualifiedName otherName = (QualifiedName)id2qname.get(id);
            if (otherName != null && !qname.equals(otherName)) {
                conflictNames.add(qname);
                /* put in by vsy so that both m1/X and m2/X are qualified */
                conflictNames.add(otherName);
            } else
                id2qname.put(id, qname);
        }

    }

    public String getShortSigName(SigExpr expr) {
        QualifiedName qname = expr.getSig();
        Id id = qname.getId();

        StringBuffer retString =
            new StringBuffer(!conflictNames.contains(qname) ? id.nodeString() : qname.nodeString());

        return retString.toString();
    }

    /*

    private String getShortSigTypeName(SigType type) {
        //return type.getSignature().getName().getId().nodeString();
        return type.toShortString();
    }*/

    private String getModelName() {
        Node node = _command;
        while (!((node == null) || node instanceof alloy.ast.Module)) {
            node = node.getParent();
        }
        Dbg.chk(node);
        return ((alloy.ast.Module)node).getName().nodeString();
    }

    private boolean isSubset(SigExpr sig) {
        if (sig.getType().size() > 1) {
            // if type is a union of types sig couldn't have been a type
            return true;
        }

        // otherwise, if it's a set of type Int, simply check if its id is INT_ID
        // otherwise check if its id is equal to that of its type's signature
        BasicType type = sig.getType().toRelationType().getBasicTypeAt(0);
	/** EMINA:  INT NOW HAS A SIG **/
	/**
        if (type instanceof IntType) {
            return (!sig.getLeafId().equals(LeafId.INT_ID));
	    } else { **/
            return !sig.getLeafId().equals(((SigType)type).getSignature().getLeafId());
	    //}
    }

    private String getModuleName(LeafExpr leaf) {
        if (leaf instanceof SigExpr) {
            // if it's the SigExpr for Int, return the focus module (because otherwise
            // it's unspecified).
	    /** EMINA:  INT NOW HAS A MODULE **/
	    /**
            if (leaf.getLeafId().equals(LeafId.INT_ID)) {
                return ((Module)_command.getParent().getParent()).getName().nodeString();
		} else { **/
                return ((SigExpr)leaf).getSig().getPath().nodeString();
		//}
        } else {
            // use first type
            RelationType relType = (RelationType)leaf.getType().getTypeIter().next();
            BasicType firstType = relType.getBasicTypeAt(0);
            Dbg.chk(firstType instanceof SigType);
            return getModuleName(((SigType)firstType).getSignature().toSigExpr());
        }
    }

    public Relation getRelation(LeafId id) {
        return (Relation)_oldLeafIdToRelation.get(id);
    }

    /**
     * @return a view of a sorted list of every LeafExpr in this instance
     */
    public List getAllLeafExprs() {
        return Collections.unmodifiableList(_oldLeafExprs);
    }

    public List getSigExprs() {
        return _oldSigExprs;
    }

    public List getSkolems() {
        return _oldSkolems;
    }

    public BasicType getBasicTypeForAtom(Atom atom) {
        return (BasicType)_atomToBasicType.get(atom);
    }

    public Relation applyFieldToAtom(LeafId fieldId, Atom atom) {
        Relation ret = (Relation) ((Map)_atomToFieldValues.get(atom)).get(fieldId);
        return (ret == null ? new Relation() : ret);
    }

    AlloyAtom getAlloyAtom(Atom a) {
        return (AlloyAtom)_atomToAlyAtom.get(a);
    }

    Set getVizElt(LeafId id) {
        return (Set)_oldLeafIdsToVizElts.get(id);
    }

    /*public Set getFieldExprsForAtom(Atom atom) {
        return (Set) _atomToFieldExprs.get(atom);
    }*/




    private StringBuffer appendXmlAtom(final StringBuffer b, final Atom a) {
        b.append("<atom name=\"");
        String path = ((SigType)_atomToBasicType.get(a)).getSignature().getName().getPath().toString();
        b.append(path + "/" + a.toString());
        b.append("\"/>");
        return b;
    }
    private StringBuffer appendXmlTuple(final StringBuffer b, final Tuple t, final boolean withTupleTags) {
        if (withTupleTags) b.append("<tuple>");
        for (final Iterator i = t.atoms(); i.hasNext(); ) {
            appendXmlAtom(b, (Atom) i.next() );
        }
        if (withTupleTags) b.append("</tuple>\n");
        return b;
    }
    private StringBuffer appendXmlValue(final StringBuffer b, final Relation r, final boolean withTupleTags) {
        //b.append("<value>\n");
        for (final Iterator tuples = r.tuples(); tuples.hasNext(); ) {
            appendXmlTuple(b, (Tuple)tuples.next(), withTupleTags );
        }
        //b.append("</value>\n");
        return b;
    }


    public String toXML() {

        StringBuffer ret = new StringBuffer();
        ret.append("<solution>");    

        // go up the ast tree until the top Specification node is found

        Node node = _command;
        while (!(node instanceof Specification)) {
            node = node.getParent();
            Dbg.chk(node, "problem generating text output -- cannot go up ast tree");
        }

        Specification spec = (Specification)node;

        // iterate through modules
        for (Iterator modIter = spec.getModules().getModuleIter(); modIter.hasNext();) {
            Module module = (Module)modIter.next();

            ret.append("\n<module name=\"" + module.getName().nodeString() + "\">\n");

            // iterate through signatures

            for (Iterator sigIter = module.getSignatures().getSignatureIter(); sigIter.hasNext();) {
                Signature sig = (Signature)sigIter.next();

                StringBuffer sigInfo = new StringBuffer();
                sigInfo.append("\n<sig name=\"" + sig.getName().getId().nodeString() + "\" ");

                if (sig.isSubset()) {
                    sigInfo.append(">\n");
                    // sig A in B+C ...

                    for (Iterator subsetIter = sig.getSubsets().getSigExprIter(); subsetIter.hasNext();) {
                        SigExpr subsetExpr = (SigExpr)subsetIter.next();
                        sigInfo.append("<in name=\"");
                        sigInfo.append(subsetExpr.getSig().getId().nodeString());
                        sigInfo.append("\"/>");
                        //if (subsetIter.hasNext()) { sigInfo.append("+"); }
                    }
                } else {

                    // sig A extends B, or just sig A

                    Iterator extendsIter = sig.getExtends().getSigExprIter();
                    if (extendsIter.hasNext()) {
                        sigInfo.append(" extends=\"");
                        sigInfo.append(((SigExpr)extendsIter.next()).getSig().getId().nodeString());
                        sigInfo.append("\" ");
                    }
                    sigInfo.append("> ");
                }
                sigInfo.append("\n");

                // add atoms of this sig
                Relation sigAtoms = getRelation(sig.getLeafId());
                //sigInfo.append("<atoms>\n");
                appendXmlValue(sigInfo, sigAtoms, false);
                sigInfo.append("\n");
                //sigInfo.append("</atoms>\n");

                // iteratore through fields

                for (Iterator declIter = sig.getDecls().getDeclIter(); declIter.hasNext();) {
                    Decl decl = (Decl)declIter.next();

                    // need to do it separately for each variable in a Decl, e.g.
                    // sig A { foo, fee: F }

                    for (Iterator varsIter = decl.getVariables().getVariableIter(); varsIter.hasNext();) {

                        Variable var = (Variable)varsIter.next();

                        sigInfo.append("<field name=\"" + var + "\"" + " arity=\"" + (decl.getExpr().getType().arity()+1) + "\">");
                        sigInfo.append("\n<type>" + decl.getExpr() + " </type> \n");
                        
                        
                        // print values in the form of A1 -> B1, A2 -> B2
                        // cluster tuples if originating from the same atom

                        // contains mappings like
                        // A1     Set("B1")
                        // A2     Set("B2", "B3")
                        // for higher-arity rels
                        // A1     Set("B1 -> C1", "B2 -> C2")

                        //Map startAtomToStrings = new HashMap();

                        Relation fieldVals = getRelation(sig.getFieldLeafId(var.nodeString()));
                        appendXmlValue(sigInfo, fieldVals, true);
                        
                        sigInfo.append("</field>\n");
                        // end var

                    }

                    // end decl
                }
                sigInfo.append("</sig>\n");
                ret.append(sigInfo);

                // end sig
            }
            ret.append("</module>\n");
            // end module

            if (modIter.hasNext()) {
                ret.append("\n<!-- ......................................................... -->\n");
            }
        }

        // add skolems

        List skolems = getSkolems();
        ret.append("\n<!-- ... skolem constants ............................................. -->\n");
        for (Iterator skolemIter = skolems.iterator(); skolemIter.hasNext();) {
            VariableExpr skolem = (VariableExpr)skolemIter.next();
            String skolemName = shortenSkolem(skolem.nodeString());
            ret.append("<skolem name=\"");
            ret.append(skolemName);
            ret.append("\">\n");
            Relation skolemVals = getRelation(skolem.getLeafId());
            appendXmlValue(ret, skolemVals, true);
            ret.append("</skolem>\n");
        }

        ret.append("</solution>");    
        //stringRep = ret.toString();
        //return stringRep;
        return legalXML(ret.toString());
    }

    private static String legalXML(String s) {
        return s.replaceAll("\"\"","''\"");
    }

}
